Search Results: "undef"

5 January 2021

Russell Coker: Weather and Boinc

I just wrote a Perl script to look at the Australian Bureau of Meteorology pages to find the current temperature in an area and then adjust BOINC settings accordingly. The Perl script (in this post after the break, which shouldn t be in the RSS feed) takes the URL of a Bureau of Meteorology observation point as ARGV[0] and parses that to find the current (within the last hour) temperature. Then successive command line arguments are of the form 24:100 and 30:50 which indicate that at below 24C 100% of CPU cores should be used and below 30C 50% of CPU cores should be used. In warm weather having a couple of workstations in a room running BOINC (or any other CPU intensive task) will increase the temperature and also make excessive noise from cooling fans. To change the number of CPU cores used the script changes /etc/boinc-client/global_prefs_override.xml and then tells BOINC to reload that config file. This code is a little ugly (it doesn t properly parse XML, it just replaces a line of text) and could fail on a valid configuration file that wasn t produced by the current BOINC code. The parsing of the BoM page is a little ugly too, it relies on the HTML code in the BoM page they could make a page that looks identical which breaks the parsing or even a page that contains the same data that looks different. It would be nice if the BoM published some APIs for getting the weather. One thing that would be good is TXT records in the DNS. DNS supports caching with specified lifetime and is designed for high throughput in aggregate. If you had a million IOT devices polling the current temperature and forecasts every minute via DNS the people running the servers wouldn t even notice the load, while a million devices polling a web based API would be a significant load. As an aside I recommend playing nice and only running such a script every 30 minutes, the BoM page seems to be updated on the half hour so I have my cron jobs running at 5 and 35 minutes past the hour. If this code works for you then that s great. If it merely acts as an inspiration for developing your own code then that s great too! BOINC users outside Australia could replace the code for getting meteorological data (or even interface to a digital thermometer). Australians who use other CPU intensive batch jobs could take the BoM parsing code and replace the BOINC related code. If you write scripts inspired by this please blog about it and comment here with a link to your blog post.
#!/usr/bin/perl
use strict;
use Sys::Syslog;
# St Kilda Harbour RMYS
# http://www.bom.gov.au/products/IDV60901/IDV60901.95864.shtml
my $URL = $ARGV[0];
open(IN, "wget -o /dev/null -O - $URL ") or die "Can't get $URL";
while(<IN>)
 
  if($_ =~ /tr class=.rowleftcolumn/)
   
    last;
   
 
sub get_data
 
  if(not $_[0] =~ /headers=.t1-$_[1]/)
   
    return undef;
   
  $_[0] =~ s/^.*headers=.t1-$_[1]..//;
  $_[0] =~ s/<.td.*$//;
  return $_[0];
 
my @datetime;
my $cur_temp -100;
while(<IN>)
 
  chomp;
  if($_ =~ /^<.tr>$/)
   
    last;
   
  my $res;
  if($res = get_data($_, "datetime"))
   
    @datetime = split(/\//, $res)
   
  elsif($res = get_data($_, "tmp"))
   
    $cur_temp = $res;
   
 
close(IN);
if($#datetime != 1 or $cur_temp == -100)
 
  die "Can't parse BOM data";
 
my ($sec,$min,$hour,$mday,$mon,$year,$wday,$yday,$isdst) = localtime();
if($mday - $datetime[0] > 1 or ($datetime[0] > $mday and $mday != 1))
 
  die "Date wrong\n";
 
my $mins;
my @timearr = split(/:/, $datetime[1]);
$mins = $timearr[0] * 60 + $timearr [1];
if($timearr[1] =~ /pm/)
 
  $mins += 720;
 
if($mday != $datetime[0])
 
  $mins += 1440;
 
if($mins + 60 < $hour * 60 + $min)
 
  die "page outdated\n";
 
my %temp_hash;
foreach ( @ARGV[1..$#ARGV] )
 
  my @tmparr = split(/:/, $_);
  $temp_hash $tmparr[0]  = $tmparr[1];
 
my @temp_list = sort(keys(%temp_hash));
my $percent = 0;
my $i;
for($i = $#temp_list; $i >= 0 and $temp_list[$i] > $cur_temp; $i--)
 
  $percent = $temp_hash $temp_list[$i] 
 
my $prefs = "/etc/boinc-client/global_prefs_override.xml";
open(IN, "<$prefs") or die "Can't read $prefs";
my @prefs_contents;
while(<IN>)
 
  push(@prefs_contents, $_);
 
close(IN);
openlog("boincmgr-cron", "", "daemon");
my @cpus_pct = grep(/max_ncpus_pct/, @prefs_contents);
my $cpus_line = $cpus_pct[0];
$cpus_line =~ s/..max_ncpus_pct.$//;
$cpus_line =~ s/^.*max_ncpus_pct.//;
if($cpus_line == $percent)
 
  syslog("info", "Temp $cur_temp" . "C, already set to $percent");
  exit 0;
 
open(OUT, ">$prefs.new") or die "Can't read $prefs.new";
for($i = 0; $i <= $#prefs_contents; $i++)
 
  if($prefs_contents[$i] =~ /max_ncpus_pct/)
   
    print OUT "   <max_ncpus_pct>$percent.000000</max_ncpus_pct>\n";
   
  else
   
    print OUT $prefs_contents[$i];
   
 
close(OUT);
rename "$prefs.new", "$prefs" or die "can't rename";
system("boinccmd --read_global_prefs_override");
syslog("info", "Temp $cur_temp" . "C, set percentage to $percent");

1 January 2021

Dmitry Shachnev: A review of endianness bugs in Qt, and how they were fixed

As you may know, I am Qt 5 maintainer in Debian. Maintaning Qt means not only bumping the version each time a new version is released, but also making sure Qt builds successfully on all architectures that are supported in Debian (and for some submodules, the automatic tests pass). An important sort of build failures are endianness specific failures. Most widely used architectures (x86_64, aarch64) are little endian. However, Debian officially supports one big endian architecture (s390x), and unofficially a few more ports are provided, such as ppc64 and sparc64. Unfortunately, Qt upstream does not have any big endian machine in their CI system, so endianness issues get noticed only when the packages fail to build on our build daemons. In the last years I have discovered and fixed some such issues in various parts of Qt, so I decided to write a post to illustrate how to write really cross-platform C/C++ code. Issue 1: the WebP image format handler (code review) The relevant code snippet is:
if (srcImage.format() != QImage::Format_ARGB32)
    srcImage = srcImage.convertToFormat(QImage::Format_ARGB32);
// ...
if (!WebPPictureImportBGRA(&picture, srcImage.bits(), srcImage.bytesPerLine()))  
    // ...
 
The code here is serializing the images into QImage::Format_ARGB32 format, and then passing the bytes into WebP s import function. With this format, the image is stored using a 32-bit ARGB format (0xAARRGGBB). This means that the bytes will be 0xBB, 0xGG, 0xRR, 0xAA or little endian and 0xAA, 0xRR, 0xGG, 0xBB on big endian. However, WebPPictureImportBGRA expects the first format on all architectures. The fix was to use QImage::Format_RGBA8888. As the QImage documentation says, with this format the order of the colors is the same on any architecture if read as bytes 0xRR, 0xGG, 0xBB, 0xAA. Issue 2: qimage_converter_map structure (code review) The code seems to already support big endian. But maybe you can spot the error?
#if Q_BYTE_ORDER == Q_LITTLE_ENDIAN
        0,
        convert_ARGB_to_ARGB_PM,
#else
        0,
        0
#endif
It is the missing comma! It is present in the little endian block, but not in the big endian one. This was fixed trivially. Issue 3: QHandle, part of Qt 3D module (code review) QHandle class uses a union that is declared as follows:
struct Data  
    quint32 m_index : IndexBits;
    quint32 m_counter : CounterBits;
    quint32 m_unused : 2;
 ;
union  
    Data d;
    quint32 m_handle;
 ;
The sizes are declared such as IndexBits + CounterBits + 2 is always equal to 32 (four bytes). Then we have a constructor that sets the values of Data struct:
QHandle(quint32 i, quint32 count)
 
    d.m_index = i;
    d.m_counter = count;
    d.m_unused = 0;
 
The value of m_handle will be different depending on endianness! So the test that was expecting a particular value with given constructor arguments was failing. I fixed it by using the following macro:
#if Q_BYTE_ORDER == Q_BIG_ENDIAN
#define GET_EXPECTED_HANDLE(qHandle) ((qHandle.index() << (qHandle.CounterBits + 2)) + (qHandle.counter() << 2))
#else /* Q_LITTLE_ENDIAN */
#define GET_EXPECTED_HANDLE(qHandle) (qHandle.index() + (qHandle.counter() << qHandle.IndexBits))
#endif
Issue 4: QML compiler (code review) The QML compiler used a helper class named LEUInt32 (based on QLEInteger) that always stored the numbers in little endian internally. This class can be safely mixed with native quint32 on little endian systems, but not on big endian. Usually the compiler would warn about type mismatch, but here the code used reinterpret_cast, such as:
quint32 *objectTable = reinterpret_cast<quint32*>(data + qmlUnit->offsetToObjects);
So this was not noticed on build time, but the compiler was crashing. The fix was trivial again, replacing quint32 with QLEUInt32. Issue 5: QModbusPdu, part of Qt Serial Bus module (code review) The code snippet is simple:
QModbusPdu::FunctionCode code = QModbusPdu::Invalid;
if (stream.readRawData((char *) (&code), sizeof(quint8)) != sizeof(quint8))
    return stream;
QModbusPdu::FunctionCode is an enum, so code is a multi-byte value (even if only one byte is significant). However, (char *) (&code) returns a pointer to the first byte of it. It is the needed byte on little endian systems, but it is the wrong byte on big endian ones! The correct fix was using a temporary one-byte variable:
quint8 codeByte = 0;
if (stream.readRawData((char *) (&codeByte), sizeof(quint8)) != sizeof(quint8))
    return stream;
QModbusPdu::FunctionCode code = (QModbusPdu::FunctionCode) codeByte;
Issue 6: qt_is_ascii (code review) This function, as the name says, checks whether a string is ASCII. It does that by splitting the string into 4-byte chunks:
while (ptr + 4 <= end)  
    quint32 data = qFromUnaligned<quint32>(ptr);
    if (data &= 0x80808080U)  
        uint idx = qCountTrailingZeroBits(data);
        ptr += idx / 8;
        return false;
     
    ptr += 4;
 
idx / 8 is the number of trailing zero bytes. However, the bytes which are trailing on little endian are actually leading on big endian! So we can use qCountLeadingZeroBits there. Issue 7: the bundled copy of tinycbor (upstream pull request) Similar to issue 5, the code was reading into the wrong byte:
if (bytesNeeded <= 2)  
    read_bytes_unchecked(it, &it->extra, 1, bytesNeeded);
    if (bytesNeeded == 2)
        it->extra = cbor_ntohs(it->extra);
 
extra has type uint16_t, so it has two bytes. When we need only one byte, we read into the wrong byte, so the resulting number is 256 times higher on big endian than it should be. Adding a temporary one-byte variable fixed it. Issue 8: perfparser, part of Qt Creator (code review) Here it is not trivial to find the issue just looking at the code:
qint32 dataStreamVersion = qToLittleEndian(QDataStream::Qt_DefaultCompiledVersion);
However the linker was producing an error:
undefined reference to QDataStream::Version qbswap(QDataStream::Version)'
On little endian systems, qToLittleEndian is a no-op, but on big endian systems, it is a template function defined for some known types. But it turns out we need to explicitly convert enum values to a simple type, so the fix was passing qint32(QDataStream::Qt_DefaultCompiledVersion) to that function. Issue 9: Qt Personal Information Management (code review) The code in test was trying to represent a number as a sequence of bytes, using reinterpret_cast:
static inline QContactId makeId(const QString &managerName, uint id)
 
    return QContactId(QStringLiteral("qtcontacts:basic%1:").arg(managerName), QByteArray(reinterpret_cast<const char *>(&id), sizeof(uint)));
 
The order of bytes will be different on little endian and big endian systems! The fix was adding this line to the beginning of the function:
id = qToLittleEndian(id);
This will cause the bytes to be reversed on big endian systems. What remains unfixed There are still some bugs, which require deeper investigation, for example: P.S. We are looking for new people to help with maintaining Qt 6. Join our team if you want to do some fun work like described above!

16 December 2020

Jonathan McDowell: DeskPi Pro + 8GB Pi 4

DeskPi Pro Raspberry Pi case Despite having worked on a number of ARM platforms I ve never actually had an ARM based development box at home. I have a Raspberry Pi B Classic (the original 256MB rev 0002 variant) a coworker gave me some years ago, but it s not what you d choose for a build machine and generally gets used as a self contained TFTP/console server for hooking up to devices under test. Mostly I ve been able to do kernel development with the cross compilers already built as part of Debian, and either use pre-built images or Debian directly when I need userland pieces. At a previous job I had a Marvell MACCHIATObin available to me, which works out as a nice platform - quad core A72 @ 2GHz with 16GB RAM, proper SATA and a PCIe slot. However they re still a bit pricey for a casual home machine. I really like the look of the HoneyComb LX2 - 16 A72 cores, up to 64GB RAM - but it s even more expensive. So when I saw the existence of the 8GB Raspberry Pi 4 I was interested. Firstly, the Pi 4 is a proper 64 bit device (my existing Pi B is ARMv6 which means it needs to run Raspbian instead of native Debian armhf), capable of running an upstream kernel and unmodified Debian userspace. Secondly the Pi 4 has a USB 3 controller sitting on a PCIe bus rather than just the limited SoC USB 2 controller. It s not SATA, but it s still a fairly decent method of attaching some storage that s faster/more reliable than an SD card. Finally 8GB RAM is starting to get to a decent amount - for a headless build box 4GB is probably generally enough, but I wanted some headroom. The Pi comes as a bare board, so I needed a case. Ideally I wanted something self contained that could take the Pi, provide a USB/SATA adaptor and take the drive too. I came across the pre-order for the DeskPi Pro, decided it was the sort of thing I was after, and ordered one towards the end of September. It finally arrived at the start of December, at which point I got round to ordering a Pi 4 from CPC. Total cost ~ 120 for the case + Pi.

The Bad First, let s get the bad parts out of the way. Broken USB port (right) I managed to break a USB port on the Desk Pi. It has a pair of forward facing ports, I plugged my wireless keyboard dongle into it and when trying to remove it the solid spacer bit in the socket broke off. I ve never had this happen to me before and I ve been using USB devices for 20 years, so I m putting the blame on a shoddy socket. The first drive I tried was an old Crucial M500 mSATA device. I have an adaptor that makes it look like a normal 2.5 drive so I used that. Unfortunately it resulted in a boot loop; the Pi would boot its initial firmware, try to talk to the drive and then reboot before even loading Linux. The DeskPi Pro comes with an m2 adaptor and I had a spare m2 drive, so I tried that and it all worked fine. This might just be power issues, but it was an unfortunate experience especially after the USB port had broken off. (Given I ended up using an M.2 drive another case option would have been the Argon ONE M.2, which is a bit more compact.)

The Annoying DeskPi Pro without rear bezel The case is a little snug; I was worried I was going to damage things as I slid it in. Additionally the construction process is a little involved. There s a good set of instructions, but there are a lot of pieces and screws involved. This includes a couple of FFC cables to join things up. I think this is because they ve attempted to make a compact case rather than allowing a little extra room, and it does have the advantage that once assembled it feels robust without anything loose in it. DeskPi Pro with rear bezel and USB3 dongle I hate the need for an external USB3 dongle to bridge from the Pi to the USB/SATA adaptor. All the cases I ve seen with an internal drive bay have to do this, because the USB3 isn t brought out internally by the Pi, but it just looks ugly to me. It s hidden at the back, but meh. Fan control is via a USB/serial device, which is fine, but it attaches to the USB C power port which defaults to being a USB peripheral. Raspbian based kernels support device tree overlays which allows easy reconfiguration to host mode, but for a Debian based system I ended up rolling my own dtb file. I changed
#include "bcm283x-rpi-usb-peripheral.dtsi"
to
#include "bcm283x-rpi-usb-host.dtsi"
in arch/arm/boot/dts/bcm2711-rpi-4-b.dts and then I did:
cpp -nostdinc -I include -I arch -undef -x assembler-with-cpp \
    arch/arm/boot/dts/bcm2711-rpi-4-b.dts > rpi4.preprocessed
dtc -I dts -O dtb rpi4.preprocessed -o bcm2711-rpi-4-b.dtb
and the resulting bcm2711-rpi-4-b.dtb file replaced the one in /boot/firmware. This isn t a necessary step if you don t want to use the cooling fan in the case, or the front USB ports, and it s not really anyone s fault, but it was an annoying extra step to have to figure out. The DeskPi came with a microSD card that was supposed to have RaspiOS already on it. It didn t, it was blank. In my case that was fine, because I wanted to use Debian, but it was a minor niggle.

The Good I used Gunnar s pre-built Pi Debian image and it Just Worked; I dd d it to the microSD as instructed and the Pi 4 came up with working wifi, video and USB enabling me to get it configured for my network. I did an apt upgrade and got updated to the Buster 10.7 release, as well as the latest 5.9 backport kernel, and everything came back without effort after a reboot. It s lovely to be able to run Debian on this device without having to futz around with self-compiled kernels. The DeskPi makes a lot of effort to route things externally. The SD slot is brought out to the front, making it easy to fiddle with the card contents without having to open the case to replace it. All the important ports are brought out to the back either through orientation of the Pi, or extenders in the case. That means the built in Pi USB ports, the HDMI sockets (conveniently converted to full size internally), an audio jack and a USB-C power port. The aforementioned USB3 dongle for the bridge to the drive is the only external thing that s annoying. Thermally things seem good too. I haven t done a full torture test yet, but with the fan off the system is sitting at about 40 C while fairly idle. Some loops in bash that push load up to above 2 get the temperature up to 46 C or so, and turning the fan on brings it down to 40 C again. It s audible, but quieter than my laptop and not annoying. I liked the way the case came with everything I needed other than the Pi 4 and a suitable disk drive. There was an included PSU (a proper USB-C PD device, UK plug), the heatsink/fan is there, the USB/SATA converter is there and even an SD card is provided (though that s just because I had a pre-order). Speaking of the SD, I only needed it for initial setup. Recent Pi 4 bootloaders are capable of booting directly from USB mass storage devices. So I upgraded using the RPi EEPROM Recovery image (which just needs extracted to the SD FAT partition, no need for anything complicated - boot with it and the screen goes all green and you know it s ok), then created a FAT partition at the start of the drive for the kernel / bootloader config and a regular EXT4 partition for root. Copies everything over, updated paths, took out the SD and it all just works happily.

Summary My main complaint is the broken USB port, which feels like the result of a cheap connector. For a front facing port expected to see more use than the rear ports I think there s a reasonable expectation of robustness. However I m an early adopter and maybe future runs will be better. Other than that I m pretty happy. The case is exactly the sort of thing I wanted; I was looking for something that would turn the Pi into a box that can sit on my desk on the network and that I don t have to worry about knocking wires out of or lots of cables hooking bits up. Everything being included made it very convenient to get up and running. I still haven t poked the Pi that hard, but first impressions are looking good for it being a trouble free ARM64 dev box in the corner, until I can justify a HoneyComb.

21 November 2020

Giovanni Mascellani: Having fun with signal handlers

As every C and C++ programmer knows far too well, if you dereference a pointer that points outside of the space mapped on your process' memory, you get a segmentation fault and your programs crashes. As far as the language itself is concerned, you don't have a second chance and you cannot know in advance whether that dereferencing operation is going to set a bomb off or not. In technical terms, you are invoking undefined behaviour, and you should never do that: you are responsible for knowing in advance if your pointers are valid, and if they are not you keep the pieces. However, turns out that most actual operating system give you a second chance, although with a lot of fine print attached. So I tried to implement a function that tries to dereference a pointer: if it can, it gives you the value; if it can't, it tells you it couldn't. Again, I stress this should never happen in a real program, except possibly for debugging (or for having fun). The prototype is
word_t peek(word_t *addr, int *success);
The function is basically equivalent to return *addr, except that if addr is not mapped it doesn't crash, and if success is not NULL it is set to 0 or 1 to indicate that addr was not mapped or mapped. If addr was not mapped the return value is meaningless. I won't explain it in detail to leave you some fun. Basically the idea is to install a handler for SIGSEGV: if the address is invalid, the handler is called, which basically fixes everything by advancing a little bit the instruction pointer, in order to skip the faulting instruction. The dereferencing instruction is written as hardcoded Assembly bytes, so that I know exactly how many bytes I need to skip. Of course this is very architecture-dependent: I wrote the i386 and amd64 variants (no x32). And I don't guarantee there are no bugs or subtelties! Another solution would have been to just parse /proc/self/maps before dereferencing and check whether the pointer is in a mapped area, but it would have suffered of a TOCTTOU problem: another thread might have changed the mappings between the time when /proc/self/maps was parsed and when the pointer was dereferenced (also, parsing that file can take a relatively long amount of time). Another less architecture-dependent but still not pure-C approach would have been to establish a setjmp before attempting the dereference and longjmp-ing back from the signal handler (but again you would need to use different setjmp contexts in different threads to exclude race conditions). Have fun! (and again, don't try this in real programs) EDIT I realized I should specify the language for source code highlighting to work decently. Now it's better! EDIT 2 I also realized that my version of peek has problems when there are other threads, because signal actions are per-process, not per-thread (as I initially thought). See the comments for a better version (though not perfect).
#define _GNU_SOURCE
#include <stdint.h>
#include <signal.h>
#include <assert.h>
#include <stdlib.h>
#include <stdio.h>
#include <ucontext.h>
#ifdef __i386__
typedef uint32_t word_t;
#define IP_REG REG_EIP
#define IP_REG_SKIP 3
#define READ_CODE __asm__ __volatile__(".byte 0x8b, 0x03\n"  /* mov (%ebx), %eax */ \
                                       ".byte 0x41\n"        /* inc %ecx */ \
                                       : "=a"(ret), "=c"(tmp) : "b"(addr), "c"(tmp));
#endif
#ifdef __x86_64__
typedef uint64_t word_t;
#define IP_REG REG_RIP
#define IP_REG_SKIP 6
#define READ_CODE __asm__ __volatile__(".byte 0x48, 0x8b, 0x03\n"  /* mov (%rbx), %rax */ \
                                       ".byte 0x48, 0xff, 0xc1\n"  /* inc %rcx */ \
                                       : "=a"(ret), "=c"(tmp) : "b"(addr), "c"(tmp));
#endif
static void segv_action(int sig, siginfo_t *info, void *ucontext)  
    (void) sig;
    (void) info;
    ucontext_t *uctx = (ucontext_t*) ucontext;
    uctx->uc_mcontext.gregs[IP_REG] += IP_REG_SKIP;
 
struct sigaction peek_sigaction =  
    .sa_sigaction = segv_action,
    .sa_flags = SA_SIGINFO,
    .sa_mask = 0,
 ;
word_t peek(word_t *addr, int *success)  
    word_t ret;
    int tmp, res;
    struct sigaction prev_act;
    res = sigaction(SIGSEGV, &peek_sigaction, &prev_act);
    assert(res == 0);
    tmp = 0;
    READ_CODE
    res = sigaction(SIGSEGV, &prev_act, NULL);
    assert(res == 0);
    if (success)  
        *success = tmp;
     
    return ret;
 
int main()  
    int success;
    word_t number = 22;
    word_t value;
    number = 22;
    value = peek(&number, &success);
    printf("%d %d\n", success, value);
    value = peek(NULL, &success);
    printf("%d %d\n", success, value);
    value = peek((word_t*)0x1234, &success);
    printf("%d %d\n", success, value);
    return 0;
 

21 September 2020

Kees Cook: security things in Linux v5.7

Previously: v5.6 Linux v5.7 was released at the end of May. Here s my summary of various security things that caught my attention: arm64 kernel pointer authentication
While the ARMv8.3 CPU Pointer Authentication (PAC) feature landed for userspace already, Kristina Martsenko has now landed PAC support in kernel mode. The current implementation uses PACIASP which protects the saved stack pointer, similar to the existing CONFIG_STACKPROTECTOR feature, only faster. This also paves the way to sign and check pointers stored in the heap, as a way to defeat function pointer overwrites in those memory regions too. Since the behavior is different from the traditional stack protector, Amit Daniel Kachhap added an LKDTM test for PAC as well. BPF LSM
The kernel s Linux Security Module (LSM) API provide a way to write security modules that have traditionally implemented various Mandatory Access Control (MAC) systems like SELinux, AppArmor, etc. The LSM hooks are numerous and no one LSM uses them all, as some hooks are much more specialized (like those used by IMA, Yama, LoadPin, etc). There was not, however, any way to externally attach to these hooks (not even through a regular loadable kernel module) nor build fully dynamic security policy, until KP Singh landed the API for building LSM policy using BPF. With this, it is possible (for a privileged process) to write kernel LSM hooks in BPF, allowing for totally custom security policy (and reporting). execve() deadlock refactoring
There have been a number of long-standing races in the kernel s process launching code where ptrace could deadlock. Fixing these has been attempted several times over the last many years, but Eric W. Biederman and Ernd Edlinger decided to dive in, and successfully landed the a series of refactorings, splitting up the problematic locking and refactoring their uses to remove the deadlocks. While he was at it, Eric also extended the exec_id counter to 64 bits to avoid the possibility of the counter wrapping and allowing an attacker to send arbitrary signals to processes they normally shouldn t be able to. slub freelist obfuscation improvements
After Silvio Cesare observed some weaknesses in the implementation of CONFIG_SLAB_FREELIST_HARDENED s freelist pointer content obfuscation, I improved their bit diffusion, which makes attacks require significantly more memory content exposures to defeat the obfuscation. As part of the conversation, Vitaly Nikolenko pointed out that the freelist pointer s location made it relatively easy to target too (for either disclosures or overwrites), so I moved it away from the edge of the slab, making it harder to reach through small-sized overflows (which usually target the freelist pointer). As it turns out, there were a few assumptions in the kernel about the location of the freelist pointer, which had to also get cleaned up. RISCV page table dumping
Following v5.6 s generic page table dumping work, Zong Li landed the RISCV page dumping code. This means it s much easier to examine the kernel s page table layout when running a debug kernel (built with PTDUMP_DEBUGFS), visible in /sys/kernel/debug/kernel_page_tables. array index bounds checking
This is a pretty large area of work that touches a lot of overlapping elements (and history) in the Linux kernel. The short version is: C is bad at noticing when it uses an array index beyond the bounds of the declared array, and we need to fix that. For example, don t do this:
int foo[5];
...
foo[8] = bar;
The long version gets complicated by the evolution of flexible array structure members, so we ll pause for a moment and skim the surface of this topic. While things like CONFIG_FORTIFY_SOURCE try to catch these kinds of cases in the memcpy() and strcpy() family of functions, it doesn t catch it in open-coded array indexing, as seen in the code above. GCC has a warning (-Warray-bounds) for these cases, but it was disabled by Linus because of all the false positives seen due to fake flexible array members. Before flexible arrays were standardized, GNU C supported zero sized array members. And before that, C code would use a 1-element array. These were all designed so that some structure could be the header in front of some data blob that could be addressable through the last structure member:
/* 1-element array */
struct foo  
    ...
    char contents[1];
 ;
/* GNU C extension: 0-element array */
struct foo  
    ...
    char contents[0];
 ;
/* C standard: flexible array */
struct foo  
    ...
    char contents[];
 ;
instance = kmalloc(sizeof(struct foo) + content_size);
Converting all the zero- and one-element array members to flexible arrays is one of Gustavo A. R. Silva s goals, and hundreds of these changes started landing. Once fixed, -Warray-bounds can be re-enabled. Much more detail can be found in the kernel s deprecation docs. However, that will only catch the visible at compile time cases. For runtime checking, the Undefined Behavior Sanitizer has an option for adding runtime array bounds checking for catching things like this where the compiler cannot perform a static analysis of the index values:
int foo[5];
...
for (i = 0; i < some_argument; i++)  
    ...
    foo[i] = bar;
    ...
 
It was, however, not separate (via kernel Kconfig) until Elena Petrova and I split it out into CONFIG_UBSAN_BOUNDS, which is fast enough for production kernel use. With this enabled, it's now possible to instrument the kernel to catch these conditions, which seem to come up with some regularity in Wi-Fi and Bluetooth drivers for some reason. Since UBSAN (and the other Sanitizers) only WARN() by default, system owners need to set panic_on_warn=1 too if they want to defend against attacks targeting these kinds of flaws. Because of this, and to avoid bloating the kernel image with all the warning messages, I introduced CONFIG_UBSAN_TRAP which effectively turns these conditions into a BUG() without needing additional sysctl settings. Fixing "additive" snprintf() usage
A common idiom in C for building up strings is to use sprintf()'s return value to increment a pointer into a string, and build a string with more sprintf() calls:
/* safe if strlen(foo) + 1 < sizeof(string) */
wrote  = sprintf(string, "Foo: %s\n", foo);
/* overflows if strlen(foo) + strlen(bar) > sizeof(string) */
wrote += sprintf(string + wrote, "Bar: %s\n", bar);
/* writing way beyond the end of "string" now ... */
wrote += sprintf(string + wrote, "Baz: %s\n", baz);
The risk is that if these calls eventually walk off the end of the string buffer, it will start writing into other memory and create some bad situations. Switching these to snprintf() does not, however, make anything safer, since snprintf() returns how much it would have written:
/* safe, assuming available <= sizeof(string), and for this example
 * assume strlen(foo) < sizeof(string) */
wrote  = snprintf(string, available, "Foo: %s\n", foo);
/* if (strlen(bar) > available - wrote), this is still safe since the
 * write into "string" will be truncated, but now "wrote" has been
 * incremented by how much snprintf() *would* have written, so "wrote"
 * is now larger than "available". */
wrote += snprintf(string + wrote, available - wrote, "Bar: %s\n", bar);
/* string + wrote is beyond the end of string, and availabe - wrote wraps
 * around to a giant positive value, making the write effectively 
 * unbounded. */
wrote += snprintf(string + wrote, available - wrote, "Baz: %s\n", baz);
So while the first overflowing call would be safe, the next one would be targeting beyond the end of the array and the size calculation will have wrapped around to a giant limit. Replacing this idiom with scnprintf() solves the issue because it only reports what was actually written. To this end, Takashi Iwai has been landing a bunch scnprintf() fixes. That's it for now! Let me know if there is anything else you think I should mention here. Next up: Linux v5.8.

2020, Kees Cook. This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 License.
CC BY-SA 4.0

1 August 2020

Utkarsh Gupta: FOSS Activites in July 2020

Here s my (tenth) monthly update about the activities I ve done in the F/L/OSS world.

Debian
This was my 17th month of contributing to Debian. I became a DM in late March last year and a DD last Christmas! \o/ Well, this month I didn t do a lot of Debian stuff, like I usually do, however, I did a lot of things related to Debian (indirectly via GSoC)! Anyway, here are the following things I did this month:

Uploads and bug fixes:

Other $things:
  • Mentoring for newcomers.
  • FTP Trainee reviewing.
  • Moderation of -project mailing list.
  • Sponsored php-twig for William, ruby-growl, ruby-xmpp4r, and uby-uniform-notifier for Cocoa, sup-mail for Iain, and node-markdown-it for Sakshi.

GSoC Phase 2, Part 2! In May, I got selected as a Google Summer of Code student for Debian again! \o/
I am working on the Upstream-Downstream Cooperation in Ruby project. The first three blogs can be found here: Also, I log daily updates at gsocwithutkarsh2102.tk. Whilst the daily updates are available at the above site^, I ll breakdown the important parts of the later half of the second month here:
  • Marc Andre, very kindly, helped in fixing the specs that were failing earlier this month. Well, the problem was with the specs, but I am still confused how so. Anyway..
  • Finished documentation of the second cop and marked the PR as ready to be reviewed.
  • David reviewed and suggested some really good changes and I fixed/tweaked that PR as per his suggestion to finally finish the last bits of the second cop, RelativeRequireToLib.
  • Merged the PR upon two approvals and released it as v0.2.0!
  • We had our next weekly meeting where we discussed the next steps and the things that are supposed to be done for the next set of cops.
  • Introduced rubocop-packaging to the outer world and requested other upstream projects to use it! It is being used by 13 other projects already!
  • Started to work on packaging-style-guide but I didn t push anything to the public repository yet.
  • Worked on refactoring the cops_documentation Rake task which was broken by the new auto-corrector API. Opened PR #7 for it. It ll be merged after the next RuboCop release as it uses CopsDocumentationGenerator class from the master branch.
  • Whilst working on autoprefixer-rails, I found something unusual. The second cop shouldn t really report offenses if the require_relative calls are from lib to lib itself. This is a false-positive. Opened issue #8 for the same.

Debian (E)LTS
Debian Long Term Support (LTS) is a project to extend the lifetime of all Debian stable releases to (at least) 5 years. Debian LTS is not handled by the Debian security team, but by a separate group of volunteers and companies interested in making it a success. And Debian Extended LTS (ELTS) is its sister project, extending support to the Jessie release (+2 years after LTS support). This was my tenth month as a Debian LTS and my first as a Debian ELTS paid contributor.
I was assigned 25.25 hours for LTS and 13.25 hours for ELTS and worked on the following things:

LTS CVE Fixes and Announcements:

ELTS CVE Fixes and Announcements:

Other (E)LTS Work:
  • Did my LTS frontdesk duty from 29th June to 5th July.
  • Triaged qemu, firefox-esr, wordpress, libmediainfo, squirrelmail, xen, openjpeg2, samba, and ldb.
  • Mark CVE-2020-15395/libmediainfo as no-dsa for Jessie.
  • Mark CVE-2020-13754/qemu as no-dsa/intrusive for Stretch and Jessie.
  • Mark CVE-2020-12829/qemu as no-dsa for Jessie.
  • Mark CVE-2020-10756/qemu as not-affected for Jessie.
  • Mark CVE-2020-13253/qemu as postponed for Jessie.
  • Drop squirrelmail and xen for Stretch LTS.
  • Add notes for tomcat8, shiro, and cacti to take care of the Stretch issues.
  • Emailed team@security.d.o and debian-lts@l.d.o regarding possible clashes.
  • Maintenance of LTS Survey on the self-hosted LimeSurvey instance. Received 1765 (just wow!) responses.
  • Attended the fourth LTS meeting. MOM here.
  • General discussion on LTS private and public mailing list.

Other(s)
Sometimes it gets hard to categorize work/things into a particular category.
That s why I am writing all of those things inside this category.
This includes two sub-categories and they are as follows.

Personal: This month I did the following things:
  • Released v0.2.0 of rubocop-packaging on RubyGems!
    It s open-sourced and the repository is here.
    Bug reports and pull requests are welcomed!
  • Released v0.1.0 of get_root on RubyGems!
    It s open-sourced and the repository is here.
  • Wrote max-word-frequency, my Rails C1M2 programming assignment.
    And made it pretty neater & cleaner!
  • Refactored my lts-dla and elts-ela scripts entirely and wrote them in Ruby so that there are no issues and no false-positives!
    Check lts-dla here and elts-ela here.
  • And finally, built my first Rails (mini) web-application!
    The repository is here. This was also a programming assignment (C1M3).
    And furthermore, hosted it at Heroku.

Open Source: Again, this contains all the things that I couldn t categorize earlier.
Opened several issues and PRs:
  • Issue #8273 against rubocop, reporting a false-positive auto-correct for Style/WhileUntilModifier.
  • Issue #615 against http reporting a weird behavior of a flaky test.
  • PR #3791 for rubygems/bundler to remove redundant bundler/setup require call from spec_helper generated by bundle gem.
  • Issue #3831 against rubygems, reporting a traceback of undefined method, rubyforge_project=.
  • Issue #238 against nheko asking for enhancement in showing the font name in the very font itself.
  • PR #2307 for puma to constrain rake-compiler to v0.9.4.
  • And finally, I joined the Cucumber organization! \o/

Thank you for sticking along for so long :) Until next time.
:wq for today.

29 April 2020

Craig Small: Sending data in a signal

The well-known kill system call has been around for decades and is used to send a signal to another process. The most common use is to terminate or kill another process by sending the KILL or TERM signal but it can be used for a form of IPC, usually around giving the other process a kick to do something. One thing that isn t as well known is besides sending a signal to a process, you can send some data to it. This can either be an integer or a pointer and uses similar semantics to the known kill and signal handler. I came across this when there was a merge request for procps. The main changes are using sigqueue instead of kill in the sender and using a signal action not a signal handler in the receiver. To illustrate this feature, I have a small set of programs called sender and receiver that will pass an integer between them. The Sender The sender program is extremely simple, use a random(ish) from time masked to two bytes, put it in the required union and send the lot to sendqueue.
# include <signal.h>
# include <stdlib.h>
# include <stdio.h>
# include <time.h>
int main(int argc, char **argv)
 
    union sigval sigval;
    pid_t pid;
    if (argc < 2   (pid = atoi(argv[1])) < 0)
	return EXIT_FAILURE;
    sigval.sival_int = time(NULL) &amp; 0xff;
    printf("sender: sending %d to PID %d\n",
        sigval.sival_int, pid);
    sigqueue(pid, SIGUSR1, sigval);
    return EXIT_SUCCESS;
 
The key lines are 13 and 16 where the random (ish) integer is stored in the sigval union and then sent to the other process with the sigqueue. The receiver The receiver just sets up the signal handler, sends its PID (so I know what to tell the sender) and sits in a sleeping loop.
# include <stdio.h>
# include <stdlib.h>
# include <sys/types.h>
# include <unistd.h>
# include <signal.h>
void signal_handler(int signum, siginfo_t *siginfo, void *ucontext)
 
    if (signum != SIGUSR1) return;
    if (siginfo->si_code != SI_QUEUE) return;
    printf("receiver: Got value %d\n",
	    siginfo->si_int);
 
int main(int argc, char **argv)
 
    pid_t pid = getpid();
    struct sigaction signal_action;
    printf("receiver: PID is %d\n", pid);
    signal_action.sa_sigaction = signal_handler;
    sigemptyset (&amp;signal_action.sa_mask);
    signal_action.sa_flags = SA_SIGINFO;
    sigaction(SIGUSR1, &amp;signal_action, NULL);
    while(1) sleep(100);
    return EXIT_SUCCESS;
 
Lines 16-26 setup the signal handler. The main difference here is SA_SIGINFO used for the signal flags and sigaction references a sa_sigaction function rather than sa_handler. We need to use a different function because the sigaction only is passed the signal number but we need more information, including the integer that the sender process stored in sigval. Lines 7-14 are the signal handler function itself. It first checks that the receiver process got the correct signal (SIGUSR1 in this case) and that we got this signal from sigqueue because the type is SI_QUEUE. Checking the type of signal is important because different signals give you different data. For example, if you signalled this process with kill then si_int is undefined. The result As a proof of concept, the results are not terribly exciting. We see the sender say what it will be sending and the receiver saying it got it. It was useful to get some results, especially when things went wrong.
$ ./receiver &amp;
[1] 370216
receiver: PID is 370216
$ ./sender 370216
sender: sending 133 to (gdPID 370216
receiver: Got value 133
Gotchas While testing the two process there was two gotchas I encountered. GDB and the siginfo structure The sigaction manual page shows a simple siginfo_t structure, however when looking at what is passed to the signal handler, it s much more complicated.
(gdb) p *siginfo
$2 =  si_signo = 10, si_errno = 0, si_code = -1, __pad0 = 0, _sifields =  _pad =  371539, 1000, 11, 32766, 0 <repeats 24 times> , _kill =  si_pid = 371539, si_uid = 1000 , _timer =  si_tid = 371539, 
      si_overrun = 1000, si_sigval =  sival_int = 11, sival_ptr = 0x7ffe0000000b , _rt =  si_pid = 371539, si_uid = 1000, si_sigval =  sival_int = 11, sival_ptr = 0x7ffe0000000b , _sigchld =  
      si_pid = 371539, si_uid = 1000, si_status = 11, si_utime = 0, si_stime = 0 , _sigfault =  si_addr = 0x3e80005ab53, si_addr_lsb = 11, _bounds =  _addr_bnd =  _lower = 0x0, _upper = 0x0 , _pkey = 0 , 
    _sigpoll =  si_band = 4294967667539, si_fd = 11 , _sigsys =  _call_addr = 0x3e80005ab53, _syscall = 11, _arch = 32766 
(gdb) p siginfo->_sifields._rt.si_sigval.sival_int
$3 = 11
So the integer is stored in a union in a structure in a structure. Much harder to find than just simply sival_int. The pointer is just a pointer So perhaps sending an integer is not enough. The sigval is a union with an integer and a pointer. Could a string be sent instead? I changed line 13 of the sender so it used a string instead of an integer.
    sigval.sival_ptr = "Hello, World!"
The receiver needed a minor adjustment to print out the string. I tried this and the receiver segmentation faulted. What was going on? The issue is the set of system calls does a simple passing of the values. So if the sender sends a pointer to a string located at 0x1234567 then the receiver will have a pointer to the same location. When the receiver tries to dereference the sival_ptr, it is pointing to memory that is not owned by it but by another process (the sender) so it segmentation faults. The solution would be to use shared memory between the processes. The signal queue would then use the pointer to the shared memory and, in theory, all would be well.

22 March 2020

Sylvestre Ledru: Some clang rebuild results (8.0.1, 9.0.1 & 10rc2)

As part of the LLVM release cycle, I am continuing rebuilding the Debian archive with clang instead of gcc to evaluate potential regressions. Processed results are available on the website: https://clang.debian.net/status.php - Now includes some fancy graphs to show the evolution
Raw logs are published on github: https://github.com/opencollab/clang.debian.net/tree/master/logs Since my last blog post on the subject (August 2017), Clang is more and more present in the tech ecosystem. It is now the compiler used to build Firefox and Chrome upstream binaries on all the supported architectures/operating systems. More architectures are supported, it has a new linker (lld), a new hybrid IR (MLIR), a lot of checkers in clang-tidy, cross-language linking with Rust, etc.

Results
Now, about Debian results, we rebuilt using 8.0.1, 9.0.1 and 10.0rc2. Results are pretty similar to what we had with previous versions: between 4 to 5% of packages are failing when gcc is replaced by clang.
Some clang rebuild results (8.0.1, 9.0.1 &amp; 10rc2)

Even if most of the software are still using gcc as compiler, we can see that clang has a positive effect on code quality. With many different kinds of errors and warnings found clang over the years, we noticed a steady decline of the number of errors. For example, the number of incorrect C/C++ main declarations has been decreasing years after years:
Some clang rebuild results (8.0.1, 9.0.1 &amp; 10rc2)

Errors found
The biggest offender is still the qmake changes which doesn't allow the used workaround (replacing /usr/bin/gcc by /usr/bin/clang) - about 250 errors. Most of these packages would probably compile fine with clang. More on the Qt bug tracker. The workaround proposed in the bug isn't applicable for us as we use the dropped-in replacement of the
The second error is still some differences in symbol generation. Unlike gcc, it seems that clang doesn't generate some symbols (or adds some). As a bunch of Debian packages are checking the list of symbols in the library (for ABI management), the build fails on purpose. For example, with libcec, the symbol _ZN10P8PLATFORM14CConditionImplD1Ev@Base 3.1.0 isn't generated anymore. I am not expecting this to be a big deal: the generated libraries probably works most of the time. More on C++ symbol management in Debian.

Current status
As previously said in a blog post, I don't think there is a strong intensive to go away from gcc for most of the Linux distributions. The big reason for BSD was the license (even if the move to the Apache 2 license wasn't received positively by some of them).
While the LLVM/clang ecosystem clearly won the tooling battle, as a C/C++ compiler, gcc is still an excellent compiler which supports more architecture and more languages.
In term of new warnings and checks, as the clang community moved the efforts in clang-tidy (which requires more complex tooling), out of the box, gcc provides a better experience (as example, see the Firefox meta bug to build with -Werror with the default warnings using gcc 9, gcc 10 and clang trunk for example).

Next steps
I see some potential next steps to decrease the number of failure:
  • Workaround the Qt/Qmake issue
  • Fix the objective-c header include issues (echo "#include <objc/objc.h>" > foo.m && clang -c foo.m is currently failing)
  • Identify why clang generates more/less symbols that gcc in the library and try to fix that
  • Rebuild the archive with clang-7 - Seems that I have some data problem

Many thanks to Lucas Nussbaum for the rebuilds.

20 November 2017

Reproducible builds folks: Reproducible Builds: Weekly report #133

Here's what happened in the Reproducible Builds effort between Sunday November 5 and Saturday November 11 2017: Upcoming events On November 17th Chris Lamb will present at Open Compliance Summit, Yokohama, Japan on how reproducible builds ensures the long-term sustainability of technology infrastructure. We plan to hold an assembly at 34C3 - hope to see you there! LEDE CI tests Thanks to the work of lynxis, Mattia and h01ger, we're now testing all LEDE packages in our setup. This is our first result for the ar71xx target: "502 (100.0%) out of 502 built images and 4932 (94.8%) out of 5200 built packages were reproducible in our test setup." - see below for details how this was achieved. Bootstrapping and Diverse Double Compilation As a follow-up of a discussion on bootstrapping compilers we had on the Berlin summit, Bernhard and Ximin worked on a Proof of Concept for Diverse Double Compilation of tinycc (aka tcc). Ximin Luo did a successful diverse-double compilation of tinycc git HEAD using gcc-7.2.0, clang-4.0.1, icc-18.0.0 and pgcc-17.10-0 (pgcc needs to triple-compile it). More variations are planned for the future, with the eventual aim to reproduce the same binaries cross-distro, and extend it to test GCC itself. Packages reviewed and fixed, and bugs filed Patches filed upstream: Patches filed in Debian: Patches filed in OpenSUSE: Reviews of unreproducible packages 73 package reviews have been added, 88 have been updated and 40 have been removed in this week, adding to our knowledge about identified issues. 4 issue types have been updated: Weekly QA work During our reproducibility testing, FTBFS bugs have been detected and reported by: diffoscope development Mattia Rizzolo uploaded version 88~bpo9+1 to stretch-backports. reprotest development reproducible-website development theunreproduciblepackage development tests.reproducible-builds.org in detail Misc. This week's edition was written by Ximin Luo, Bernhard M. Wiedemann, Chris Lamb and Holger Levsen & reviewed by a bunch of Reproducible Builds folks on IRC & the mailing lists.

13 November 2017

Markus Koschany: My Free Software Activities in October 2017

Welcome to gambaru.de. Here is my monthly report that covers what I have been doing for Debian. If you re interested in Java, Games and LTS topics, this might be interesting for you. Debian Games Debian Java Debian LTS This was my twentieth month as a paid contributor and I have been paid to work 19 hours on Debian LTS, a project started by Rapha l Hertzog. I will catch up with the remaining 1,75 hours in November. In that time I did the following: Misc Thanks for reading and see you next time.

12 October 2017

Joachim Breitner: Isabelle functions: Always total, sometimes undefined

Often, when I mention how things work in the interactive theorem prover [Isabelle/HOL] (in the following just Isabelle 1) to people with a strong background in functional programming (whether that means Haskell or Coq or something else), I cause confusion, especially around the issue of what is a function, are function total and what is the business with undefined. In this blog post, I want to explain some these issues, aimed at functional programmers or type theoreticians. Note that this is not meant to be a tutorial; I will not explain how to do these things, and will focus on what they mean.

HOL is a logic of total functions If I have a Isabelle function f :: a b between two types a and b (the function arrow in Isabelle is , not ), then by definition of what it means to be a function in HOL whenever I have a value x :: a, then the expression f x (i.e. f applied to x) is a value of type b. Therefore, and without exception, every Isabelle function is total. In particular, it cannot be that f x does not exist for some x :: a. This is a first difference from Haskell, which does have partial functions like
spin :: Maybe Integer -> Bool
spin (Just n) = spin (Just (n+1))
Here, neither the expression spin Nothing nor the expression spin (Just 42) produce a value of type Bool: The former raises an exception ( incomplete pattern match ), the latter does not terminate. Confusingly, though, both expressions have type Bool. Because every function is total, this confusion cannot arise in Isabelle: If an expression e has type t, then it is a value of type t. This trait is shared with other total systems, including Coq. Did you notice the emphasis I put on the word is here, and how I deliberately did not write evaluates to or returns ? This is because of another big source for confusion:

Isabelle functions do not compute We (i.e., functional programmers) stole the word function from mathematics and repurposed it2. But the word function , in the context of Isabelle, refers to the mathematical concept of a function, and it helps to keep that in mind. What is the difference?
  • A function a b in functional programming is an algorithm that, given a value of type a, calculates (returns, evaluates to) a value of type b.
  • A function a b in math (or Isabelle) associates with each value of type a a value of type b.
For example, the following is a perfectly valid function definition in math (and HOL), but could not be a function in the programming sense:
definition foo :: "(nat   real)   real" where
  "foo seq = (if convergent seq then lim seq else 0)"
This assigns a real number to every sequence, but it does not compute it in any useful sense. From this it follows that

Isabelle functions are specified, not defined Consider this function definition:
fun plus :: "nat   nat   nat"  where
   "plus 0       m = m"
   "plus (Suc n) m = Suc (plus n m)"
To a functional programmer, this reads
plus is a function that analyses its first argument. If that is 0, then it returns the second argument. Otherwise, it calls itself with the predecessor of the first argument and increases the result by one.
which is clearly a description of a computation. But to Isabelle, the above reads
plus is a binary function on natural numbers, and it satisfies the following two equations:
And in fact, it is not so much Isabelle that reads it this way, but rather the fun command, which is external to the Isabelle logic. The fun command analyses the given equations, constructs a non-recursive definition of plus under the hood, passes that to Isabelle and then proves that the given equations hold for plus. One interesting consequence of this is that different specifications can lead to the same functions. In fact, if we would define plus' by recursing on the second argument, we d obtain the the same function (i.e. plus = plus' is a theorem, and there would be no way of telling the two apart).

Termination is a property of specifications, not functions Because a function does not evaluate, it does not make sense to ask if it terminates. The question of termination arises before the function is defined: The fun command can only construct plus in a way that the equations hold if it passes a termination check very much like Fixpoint in Coq. But while the termination check of Fixpoint in Coq is a deep part of the basic logic, in Isabelle it is simply something that this particular command requires for its internal machinery to go through. At no point does a termination proof of the function exist as a theorem inside the logic. And other commands may have other means of defining a function that do not even require such a termination argument! For example, a function specification that is tail-recursive can be turned in to a function, even without a termination proof: The following definition describes a higher-order function that iterates its first argument f on the second argument x until it finds a fixpoint. It is completely polymorphic (the single quote in 'a indicates that this is a type variable):
partial_function (tailrec)
  fixpoint :: "('a   'a)   'a   'a"
where
  "fixpoint f x = (if f x = x then x else fixpoint f (f x))"
We can work with this definition just fine. For example, if we instantiate f with ( x. x-1), we can prove that it will always return 0:
lemma "fixpoint (  n . n - 1) (n::nat) = 0"
  by (induction n) (auto simp add: fixpoint.simps)
Similarly, if we have a function that works within the option monad (i.e. Maybe in Haskell), its specification can always be turned into a function without an explicit termination proof here one that calculates the Collatz sequence:
partial_function (option) collatz :: "nat   nat list option"
 where "collatz n =
        (if n = 1 then Some [n]
         else if even n
           then do   ns <- collatz (n div 2);    Some (n # ns)  
           else do   ns <- collatz (3 * n + 1);  Some (n # ns) )"
Note that lists in Isabelle are finite (like in Coq, unlike in Haskell), so this function returns a list only if the collatz sequence eventually reaches 1. I expect these definitions to make a Coq user very uneasy. How can fixpoint be a total function? What is fixpoint ( n. n+1)? What if we run collatz n for a n where the Collatz sequence does not reach 1?3 We will come back to that question after a little detour

HOL is a logic of non-empty types Another big difference between Isabelle and Coq is that in Isabelle, every type is inhabited. Just like the totality of functions, this is a very fundamental fact about what HOL defines to be a type. Isabelle gets away with that design because in Isabelle, we do not use types for propositions (like we do in Coq), so we do not need empty types to denote false propositions. This design has an important consequence: It allows the existence of a polymorphic expression that inhabits any type, namely
undefined :: 'a
The naming of this term alone has caused a great deal of confusion for Isabelle beginners, or in communication with users of different systems, so I implore you to not read too much into the name. In fact, you will have a better time if you think of it as arbitrary or, even better, unknown. Since undefined can be instantiated at any type, we can instantiate it for example at bool, and we can observe an important fact: undefined is not an extra value besides the usual ones . It is simply some value of that type, which is demonstrated in the following lemma:
lemma "undefined = True   undefined = False" by auto
In fact, if the type has only one value (such as the unit type), then we know the value of undefined for sure:
lemma "undefined = ()" by auto
It is very handy to be able to produce an expression of any type, as we will see as follows

Partial functions are just underspecified functions For example, it allows us to translate incomplete function specifications. Consider this definition, Isabelle s equivalent of Haskell s partial fromJust function:
fun fromSome :: "'a option   'a" where
  "fromSome (Some x) = x"
This definition is accepted by fun (albeit with a warning), and the generated function fromSome behaves exactly as specified: when applied to Some x, it is x. The term fromSome None is also a value of type 'a, we just do not know which one it is, as the specification does not address that. So fromSome None behaves just like undefined above, i.e. we can prove
lemma "fromSome None = False   fromSome None = True" by auto
Here is a small exercise for you: Can you come up with an explanation for the following lemma:
fun constOrId :: "bool   bool" where
  "constOrId True = True"
lemma "constOrId = ( _.True)   constOrId = ( x. x)"
  by (metis (full_types) constOrId.simps)
Overall, this behavior makes sense if we remember that function definitions in Isabelle are not really definitions, but rather specifications. And a partial function definition is simply a underspecification. The resulting function is simply any function hat fulfills the specification, and the two lemmas above underline that observation.

Nonterminating functions are also just underspecified Let us return to the puzzle posed by fixpoint above. Clearly, the function seen as a functional program is not total: When passed the argument ( n. n + 1) or ( b. b) it will loop forever trying to find a fixed point. But Isabelle functions are not functional programs, and the definitions are just specifications. What does the specification say about the case when f has no fixed-point? It states that the equation fixpoint f x = fixpoint f (f x) holds. And this equation has a solution, for example fixpoint f _ = undefined. Or more concretely: The specification of the fixpoint function states that fixpoint ( b. b) True = fixpoint ( b. b) False has to hold, but it does not specify which particular value (True or False) it should denote any is fine.

Not all function specifications are ok At this point you might wonder: Can I just specify any equations for a function f and get a function out of that? But rest assured: That is not the case. For example, no Isabelle command allows you define a function bogus :: () nat with the equation bogus () = Suc (bogus ()), because this equation does not have a solution. We can actually prove that such a function cannot exist:
lemma no_bogus: "  bogus. bogus () = Suc (bogus ())" by simp
(Of course, not_bogus () = not_bogus () is just fine )

You cannot reason about partiality in Isabelle We have seen that there are many ways to define functions that one might consider partial . Given a function, can we prove that it is not partial in that sense? Unfortunately, but unavoidably, no: Since undefined is not a separate, recognizable value, but rather simply an unknown one, there is no way of stating that A function result is not specified . Here is an example that demonstrates this: Two partial functions (one with not all cases specified, the other one with a self-referential specification) are indistinguishable from the total variant:
fun partial1 :: "bool   unit" where
  "partial1 True = ()"
partial_function (tailrec) partial2 :: "bool   unit" where
  "partial2 b = partial2 b"
fun total :: "bool   unit" where
  "total True = ()"
  "total False = ()"
lemma "partial1 = total   partial2 = total" by auto
If you really do want to reason about partiality of functional programs in Isabelle, you should consider implementing them not as plain HOL functions, but rather use HOLCF, where you can give equational specifications of functional programs and obtain continuous functions between domains. In that setting, () and partial2 = total. We have done that to verify some of HLint s equations.

You can still compute with Isabelle functions I hope by this point, I have not scared away anyone who wants to use Isabelle for functional programming, and in fact, you can use it for that. If the equations that you pass to fun are a reasonable definition for a function (in the programming sense), then these equations, used as rewriting rules, will allow you to compute that function quite like you would in Coq or Haskell. Moreover, Isabelle supports code extraction: You can take the equations of your Isabelle functions and have them expored into Ocaml, Haskell, Scala or Standard ML. See Concon for a conference management system with confidentially verified in Isabelle. While these usually are the equations you defined the function with, they don't have to: You can declare other proved equations to be used for code extraction, e.g. to refine your elegant definitions to performant ones. Like with code extraction from Coq to, say, Haskell, the adequacy of the translations rests on a moral reasoning foundation. Unlike extraction from Coq, where you have an (unformalized) guarantee that the resulting Haskell code is terminating, you do not get that guarantee from Isabelle. Conversely, this allows you do reason about and extract non-terminating programs, like fixpoint, which is not possible in Coq. There is currently ongoing work about verified code generation, where the code equations are reflected into a deep embedding of HOL in Isabelle that would allow explicit termination proofs.

Conclusion We have seen how in Isabelle, every function is total. Function declarations have equations, but these do not define the function in an computational sense, but rather specify them. Because in HOL, there are no empty types, many specifications that appear partial (incomplete patterns, non-terminating recursion) have solutions in the space of total functions. Partiality in the specification is no longer visible in the final product.

PS: Axiom undefined in Coq This section is speculative, and an invitation for discussion. Coq already distinguishes between types used in programs (Set) and types used in proofs Prop. Could Coq ensure that every t : Set is non-empty? I imagine this would require additional checks in the Inductive command, similar to the checks that the Isabelle command datatype has to perform4, and it would disallow Empty_set. If so, then it would be sound to add the following axiom
Axiom undefined : forall (a : Set), a.
wouldn't it? This axiom does not have any computational meaning, but that seems to be ok for optional Coq axioms, like classical reasoning or function extensionality. With this in place, how much of what I describe above about function definitions in Isabelle could now be done soundly in Coq. Certainly pattern matches would not have to be complete and could sport an implicit case _ undefined. Would it help with non-obviously terminating functions? Would it allow a Coq command Tailrecursive that accepts any tailrecursive function without a termination check?

  1. Isabelle is a metalogical framework, and other logics, e.g. Isabelle/ZF, behave differently. For the purpose of this blog post, I always mean Isabelle/HOL.
  2. Isabelle is a metalogical framework, and other logics, e.g. Isabelle/ZF, behave differently. For the purpose of this blog post, I always mean Isabelle/HOL.
  3. Let me know if you find such an n. Besides n = 0.
  4. Like fun, the constructions by datatype are not part of the logic, but create a type definition from more primitive notions that is isomorphic to the specified data type.

13 September 2017

Reproducible builds folks: Reproducible Builds: Weekly report #124

Here's what happened in the Reproducible Builds effort between Sunday September 3 and Saturday September 9 2017: Media coverage GSoC and Outreachy updates Debian will participate in this year's Outreachy initiative and the Reproducible Builds is soliciting mentors and students to join this round. For more background please see the following mailing list posts: 1, 2 & 3. Reproduciblity work in Debian In addition, the following NMUs were accepted: Reproduciblity work in other projects Patches sent upstream: Packages reviewed and fixed, and bugs filed Reviews of unreproducible packages 3 package reviews have been added, 2 have been updated and 2 have been removed in this week, adding to our knowledge about identified issues. Weekly QA work During our reproducibility testing, FTBFS bugs have been detected and reported by: diffoscope development Development continued in git, including the following contributions: Mattia Rizzolo also uploaded the version 86 released last week to stretch-backports. reprotest development tests.reproducible-builds.org Misc. This week's edition was written by Bernhard M. Wiedemann, Chris Lamb, Holger Levsen, Mattia Rizzolo & reviewed by a bunch of Reproducible Builds folks on IRC & the mailing lists.

23 July 2017

Gregor Herrmann: RC bugs 2017/08-29

long time no blog post. & the stretch release happened without many RC bug fixes from me; in practice, the auto-removals are faster & more convenient. what I nevertheless did in the last months was to fix RC bugs in pkg-perl packages (it still surprises me how fast rotting & constantly moving code is); prepare RC bug fixes for jessie (also for pkg-perl packages); & in the last weeks provide patches & carry out NMUs for perl packages as part of the ongoing perl 5.26 transition.

14 June 2017

Steve Kemp: Porting pfctl to Linux

If you have a bunch of machines running OpenBSD for firewalling purposes, which is pretty standard, you might start to use source-control to maintain the rulesets. You might go further, and use some kind of integration testing to deploy changes from your revision control system into production. Of course before you deploy any pf.conf file you need to test that the file contents are valid/correct. If your integration system doesn't run on OpenBSD though you have a couple of choices: I looked at this last year and got pretty far, but then got distracted. So the other day I picked it up again. It turns out that if you're patient it's not hard to use bison to generate some C code, then glue it together such that you can validate your firewall rules on a Linux system.
  deagol ~/pf.ctl $ ./pfctl ./pf.conf
  ./pf.conf:298: macro 'undefined_variable' not defined
  ./pf.conf:298: syntax error
Unfortunately I had to remove quite a lot of code to get the tool to compile, which means that while some failures like that above are caught others are missed. The example above reads:
vlans=" vlan1,vlan2 "
..
pass out on $vlans proto udp from $undefined_variable
Unfortunately the following line does not raise an error:
pass out on vlan12 inet proto tcp from <unknown> to $http_server port  80,443 
That comes about because looking up the value of the table named unknown just silently fails. In slowly removing more and more code to make it compile I lost the ability to keep track of table definitions - both their names and their values - Thus the fetching of a table by name has become a NOP, and a bogus name will result in no error. Now it is possible, with more care, that you could use a hashtable library, or similar, to simulate these things. But I kinda stalled, again. (Similar things happen with fetching a proto by name, I just hardcoded inet, gre, icmp, icmp6, etc. Things that I'd actually use.) Might be a fun project for somebody with some time anyway! Download the OpenBSD source, e.g. from a github mirror - yeah, yeah, but still. CVS? No thanks! - Then poke around beneath sbin/pfctl/. The main file you'll want to grab is parse.y, although you'll need to setup a bunch of headers too, and write yourself a Makefile. Here's a hint:
  deagol ~/pf.ctl $ tree
  .
    inc
      net
        pfvar.h
      queue.h
      sys
          _null.h
          refcnt.h
          tree.h
    Makefile
    parse.y
    pf.conf
    pfctl.h
    pfctl_parser.h
    y.tab.c
  3 directories, 11 files

31 May 2017

Chris Lamb: Free software activities in May 2017

Here is my monthly update covering what I have been doing in the free software world (previous month):
Reproducible builds

Whilst anyone can inspect the source code of free software for malicious flaws, most software is distributed pre-compiled to end users. The motivation behind the Reproducible Builds effort is to permit verification that no flaws have been introduced either maliciously or accidentally during this compilation process by promising identical results are always generated from a given source, thus allowing multiple third-parties to come to a consensus on whether a build was compromised. (I have generously been awarded a grant from the Core Infrastructure Initiative to fund my work in this area.) This month I:
I also made the following changes to our tooling:
diffoscope

diffoscope is our in-depth and content-aware diff utility that can locate and diagnose reproducibility issues.

  • Don't fail when run under perversely-recursive input files. (#780761).

strip-nondeterminism

strip-nondeterminism is our tool to remove specific non-deterministic results from a completed build.

  • Move from verbose_print to nonquiet_print so we print when normalising a file. This is so we can start to target the removal of strip-nondeterminism itself.
  • Only print log messages by default if the file was actually modified. (#863033)
  • Update package long descriptions to clarify that the tool itself is a temporary workaround. (#862029)


Debian My activities as the current Debian Project Leader are covered in my "Bits from the DPL" email to the debian-devel-announce list. However, I:
  • Represented Debian at the OSCAL 2017 in Tirana, Albania.
  • Attended the Reproducible Builds hackathon in Hamburg, Germany. (Report)
  • Finally, I attended Debian SunCamp 2017 in Lloret de Mar in Catalonia, Spain.

Patches contributed
  • xarchiver: Adding files to .tar.xz deletes existing content. (#862593)
  • screen-message: Please invert the default colours. (#862056)
  • fontconfig: fc-cache returns with exit code 0 on 256 errors. (#863427)
  • quadrapassel: Segfaults when unpausing a paused finished game. (#863106)
  • camping: Broken symlink. (#861040)
  • dns-root-data: Does not build if /bin/sh is Bash. (#862252)
  • dh-python: bit.ly link doesn't work anymore. (#863074)

Debian LTS

This month I have been paid to work 18 hours on Debian Long Term Support (LTS). In that time I did the following:
  • "Frontdesk" duties, triaging CVEs, adding links to upstream patches, etc.
  • Issued DLA 930-1 fixing a remote application crash vulnerability in libxstream-java, a Java library to serialize objects to XML and back again
  • Issued DLA 935-1 correcting a local denial of service vulnerability in lxterminal, the terminal emulator for the LXDE desktop environment.
  • Issued DLA 940-1 to remedy an issue in sane-backends which allowed remote attackers to obtain sensitive memory information via a crafted SANE_NET_CONTROL_OPTION packet.
  • Issued DLA 943-1 for the deluge bittorrent client to fix a directory traversal attack vulnerability in the web user interface.
  • Issued DLA 949-1 fixing an integer signedness error in the miniupnpc UPnP client that could allow remote attackers to cause a denial of service attack.
  • Issued DLA 959-1 for the libical calendaring library. A use-after-free vulnerability could allow remote attackers could cause a denial of service and possibly read heap memory via a specially crafted .ICS file.

Uploads
  • redis (3:3.2.9-1) New upstream release.
  • python-django:
    • 1:1.11.1-1 New upstream minor release.
    • 1:1.11.1-2 & 1:1.11.1-3 Add missing Build-Depends on libgdal-dev due to new GIS tests.
  • docbook-to-man:
    • 1:2.0.0-36 Adopt package. Apply a patch to prevent undefined behaviour caused by a memcpy(3) parameter overlap. (#842635, #858389)
    • 1:2.0.0-37 Install manpages using debian/docbook-to-man.manpages over manual calls.
  • installation-birthday Initial upload and misc. subsequent fixes.
  • bfs:
    • 1.0-3 Fix FTBFS on hurd-i386. (#861569)
    • 1.0.1-1 New upstream release & correct debian/watch file.

I also made the following non-maintainer uploads (NMUs):
  • ca-certificates (20161130+nmu1) Remove StartCom and WoSign certificates as they are now untrusted by the major browser vendors. (#858539)
  • sane-backends (1.0.25-4.1) Correct missing error handler in (generated) prerm script. (#862334)
  • seqan2 (2.3.1+dfsg-3.1) Fix broken /usr/bin/splazers symlink on 32-bit architectures. (#863669)
  • jackeq (0.5.9-2.1) Fix a segmentation fault caused by passing a truncated pointer instead of a GtkType. (#863416)
  • kluppe (0.6.20-1.1) Fix segmentation fault at startup. (#863421)
  • coyim (0.3.7-2.1) Skip tests that require internet access to avoid FTBFS. (#863414)
  • pavuk (0.9.35-6.1) Fix segmentation fault when opening "Limitations" window. (#863492)
  • porg (2:0.10-1.1) Fix broken LD_PRELOAD path. (#863495)
  • timemachine (0.3.3-2.1) Fix two segmentation faults caused by truncated pointers. (#863420)

Debian bugs filed
  • acct: Docs incorrectly installed to "accounting.html" directory. (#862180)
  • git-hub: Does not work with 2FA-enabled accounts. (#863265)
  • libwibble: Homepage and Vcs-Darcs fields are outdated. (#861673)



I additionally filed 2 bugs for packages that access the internet during build against flower and r-bioc-gviz.


I also filed 6 FTBFS bugs against cronutils, isoquery, libgnupg-interface-perl, maven-plugin-tools, node-dateformat, password-store & simple-tpm-pk11.

FTP Team

As a Debian FTP assistant I ACCEPTed 105 packages: boinc-app-eah-brp, debug-me, e-mem, etcd, fdroidcl, firejail, gcc-6-cross-ports, gcc-7-cross-ports, gcc-defaults, gl2ps, gnome-software, gnupg2, golang-github-dlclark-regexp2, golang-github-dop251-goja, golang-github-nebulouslabs-fastrand, golang-github-pkg-profile, haskell-call-stack, haskell-foundation, haskell-nanospec, haskell-parallel-tree-search, haskell-posix-pty, haskell-protobuf, htmlmin, iannix, libarchive-cpio-perl, libexternalsortinginjava-java, libgetdata, libpll, libtgvoip, mariadb-10.3, maven-resolver, mysql-transitional, network-manager, node-async-each, node-aws-sign2, node-bcrypt-pbkdf, node-browserify-rsa, node-builtin-status-codes, node-caseless, node-chokidar, node-concat-with-sourcemaps, node-console-control-strings, node-create-ecdh, node-create-hash, node-create-hmac, node-cryptiles, node-dot, node-ecc-jsbn, node-elliptic, node-evp-bytestokey, node-extsprintf, node-getpass, node-gulp-coffee, node-har-schema, node-har-validator, node-hawk, node-jsprim, node-memory-fs, node-pbkdf2, node-performance-now, node-set-immediate-shim, node-sinon-chai, node-source-list-map, node-stream-array, node-string-decoder, node-stringstream, node-verror, node-vinyl-sourcemaps-apply, node-vm-browserify, node-webpack-sources, node-wide-align, odil, onionshare, opensvc, otb, perl, petsc4py, pglogical, postgresql-10, psortb, purl, pymodbus, pymssql, python-decouple, python-django-rules, python-glob2, python-ncclient, python-parse-type, python-prctl, python-sparse, quoin-clojure, quorum, r-bioc-genomeinfodbdata, radlib, reprounzip, rustc, sbt-test-interface, slepc4py, slick-greeter, sparse, te923con, trabucco, traildb, typescript-types & writegood-mode. I additionally filed 6 RC bugs against packages that had incomplete debian/copyright files against: libgetdata, odil, opensvc, python-ncclient, radlib and reprounzip.

3 April 2017

Dirk Eddelbuettel: RApiDatetime 0.0.3

A brown bag bug fix release 0.0.3 of RApiDatetime is now on CRAN. RApiDatetime provides six entry points for C-level functions of the R API for Date and Datetime calculations. The functions asPOSIXlt and asPOSIXct convert between long and compact datetime representation, formatPOSIXlt and Rstrptime convert to and from character strings, and POSIXlt2D and D2POSIXlt convert between Date and POSIXlt datetime. These six functions are all fairly essential and useful, but not one of them was previously exported by R. I left two undefined variables in calls in the exported header file; this only become an issue once I actually tried accessing the API from another package as I am now doing in anytime.

Changes in RApiDatetime version 0.0.3 (2017-04-02)
  • Correct two simple copy-and-paste errors in RApiDatetime.h
  • Also enable registration in useDynLib, and explicitly export known and documented R access functions provided for testing

Courtesy of CRANberries, there is a comparison to the previous release. More information is on the rapidatetime page. For questions or comments please use the issue tracker off the GitHub repo.

This post by Dirk Eddelbuettel originated on his Thinking inside the box blog. Please report excessive re-aggregation in third-party for-profit settings.

20 February 2017

Petter Reinholdtsen: Detect OOXML files with undefined behaviour?

I just noticed the new Norwegian proposal for archiving rules in the goverment list ECMA-376 / ISO/IEC 29500 (aka OOXML) as valid formats to put in long term storage. Luckily such files will only be accepted based on pre-approval from the National Archive. Allowing OOXML files to be used for long term storage might seem like a good idea as long as we forget that there are plenty of ways for a "valid" OOXML document to have content with no defined interpretation in the standard, which lead to a question and an idea. Is there any tool to detect if a OOXML document depend on such undefined behaviour? It would be useful for the National Archive (and anyone else interested in verifying that a document is well defined) to have such tool available when considering to approve the use of OOXML. I'm aware of the officeotron OOXML validator, but do not know how complete it is nor if it will report use of undefined behaviour. Are there other similar tools available? Please send me an email if you know of any such tool.

12 February 2017

Shirish Agarwal: Density and accessibility

Around 2 decades back and a bit more I was introduced to computers. The top-line was 386DX which was mainly used as fat servers and some lucky institutions had the 386SX where IF we were lucky we could be able to play some games on it. I was pretty bad at Prince of Persia or most of the games of the era as most of the games depended on lightning reflexes which I didn t possess. Then 1997 happened and I was introduced to GNU/Linux but my love of/for games still continued even though I was bad at most of them. The only saving grace was turn-based RPG s (role-playing games) which didn t have permadeath, so you could plan your next move. Sometimes a wrong decision would lead to getting a place from where it was impossible to move further. As the decision was taken far far break which lead to the tangent, the only recourse was to replay the game which eventually lead to giving most of those kind of games. Then in/around 2000 Maxis came out with Sims. This was the time where I bought my first Pentium. I had never played a game which had you building stuff, designing stuff, no violence and the whole idea used to be about balancing priorities of trying to get new stuff, go to work, maintain relationships and still make sure you are eating, sleeping, have a good time. While I might have spent probably something close to 500 odd hours in the game or even more so, I spent the least amount of time in building the house. It used to be 4 4 when starting (you don t have much of in-game money and other stuff you wanted to buy as well) to 8 8 or at the very grand 12 12. It was only the first time I spent time trying to figure out where the bathroom should be, where the kitchen should, where the bedroom should be and after that I could do that blind-folded. The idea behind my house-design used to be simplicity, efficient (for my character). I used to see other people s grand creations of their houses and couldn t understand why they made such big houses. Now few days back, I saw few episodes of a game called Stranded Deep . The story, plot is simple. You, the player are going in a chartered plane and suddenly lightning strikes ( game trope as today s aircrafts are much better able to deal with lightning strikes) and our hero or heroine washes up on a beach with raft with the barest of possessions. Now the whole game is based upon him/her trying to survive, once you get the hang of the basic mechanics and you know what is to be done, you can do it. The only thing the game doesn t have is farming but as the game has unlimited procedural world, you just paddle or with boat motor go island hopping and take all that what you need. What was interesting to me was seeing a gamer putting so much time and passion in making a house. When I was looking at that video, I realized that maybe because I live in a dense environment, even the designs we make either of houses or anything else is more to try to get more and more people rather than making sure that people are happy which leads to my next sharing. Couple of days back, I read Virali Modi s account of how she was molested three times when trying to use Indian Railways. She made a petition on change.org While I do condemn the molestation as it s an affront against individual rights, freedom, liberty, free movement, dignity. Few of the root causes as pointed out by her, for instance the inability or non-preference to give differently-abled people the right to board first as well as awaiting to see that everybody s boarded properly before starting the train are the most minimum steps that Indian Railways could take without spending even a paise. The same could be told/shared about sensitizing people, although I have an idea of why does Indian Railway not employ women porters or women attendants for precisely this job. I accompanied a blind gentleman friend few times on Indian Railways and let me tell you, it was one of the most unpleasant experiences. The bogies which is given to them is similar or even less than what you see in unreserved compartments. The toilets were/are smelly, the gap between the station and the train was/is considerable for everybody from blind people, differently-abled people, elderly people as well. This is one of the causes of accidents which happen almost every day on Indian Railways. I also learnt that especially for blind people they are looking for a sort of low-frequency whistle/noise which tells them the disabled coupe/bogie/coach will come at a specific spot in the Station. In a platform which could have anything between 1500-2000 people navigating it wouldn t be easy. I don t know about other places but Indian Railway Stations need to learn a lot to make it a space for differently abled to navigate by themselves. Pune Station operates (originating or passing through) around 200 odd trains, with exceptions of all the specials and weekly trains that ply through, adding those would probably another 5-10 trains to the mix. Each train carries anywhere between 750-1000 odd people so roughly anywhere between 15-20 million pass through Pune Railway Station daily. Even if we take conservative estimates of around 5% of the public commuting from Pune, it would mean around 750,000 people travelling daily. Pune Railway Station has 6 stations and if I spread them equally it would come to around 100,000 people on one platform in 24 hours. Divide that equally by 24 hours and it comes to 4,160 people per hour. Now you take those figures and you see the Pune platforms are under severe pressure. I have normalized many figures. For instance, just like airports, even in railways, there are specific timings where more trains come and go. From morning 0500 hrs to late night 2300 hrs. there would be lot many trains, whereas the graveyard shifts would have windows where maintenance of tracks and personnel takes place. I dunno if people can comprehend 4000 odd people on the platform. Add to that you usually arrive at least an hour or two before a train departs even if you are a healthy person as Indian Railways has a habit of changing platforms of trains at the last minute. So if you a differently abled person with some luggage for a long-distance train, the problems just multiply. See drag accidents because of gap between railway bogies and platforms. The width of the entrance to the bogie is probably between 30-40 inches but the design is such that 5-10 inches are taken on each side. I remembered the last year, our current Prime Minister, Mr. Narendra Modi had launched Accessible Campaign with great fanfare and we didn t hear anything much after that. Unfortunately, the site itself has latency and accessibility issues, besides not giving any real advice even if a person wants to know what building norms should one follow if one wants to make an area accessible. This was easily seen by last year s audit in Delhi as well as other places. A couple of web-searches later, I landed up at a Canadian site to have some idea about the width of the wheelchair itself as well as additional room to manoeuvre. Unfortunately, the best or the most modern coaches/bogies that Indian Railways has to offer are the LHB Bogies/Coaches. Now while the Coaches/Bogies by themselves are a big improvement from the ICF Coaches which we still have and use, if you read the advice and directions shared on the Canadian site, the coaches are far from satisfactory for people who are wheel-chair bound. According to Government s own census records, 0.6% of the population have movement issues. Getting all the differently-abled people together, it comes between 2, 2.5% of the population which is quite a bit. If 2-3 people out of every 100 people are differently-abled then we need to figure out something for them.While I don t have any ideas as to how we could improve the surroundings, it is clear that we need the change. While I was thinking,dreaming,understanding some of the nuances inadvertently, my attention/memories shifted to my toilet experiences at both Mumbai and the Doha Airport. As had shared then, had been pleasantly surprised to see that both in Mumbai Airport as well as the Doha Airport, the toilets were pretty wide, a part of me was happy and a part of me was seeing the added space as wastefulness. With the understanding of needs of differently-abled people it started to make whole lot of sense. I don t remember if I had shared then or not. Although am left wondering where they go for loo in the aircraft. The regular toilets are a tight fit for obese people, I am guessing aircrafts have toilets for differently-abled people as well. Looking back at last year s conference, we had 2-3 differently-abled people. I am just guessing that it wouldn t have been a pleasant experience for them. For instance, where we were staying, at UCT it had stairs, no lifts so by default they probably were on ground-floor. Then where we were staying and where most of the talks were about a few hundred metres away and the shortest distance were by stairs, the round-about way was by road but had vehicles around so probably not safe that way as well. I am guessing they had to be dependant on other people to figure out things. There were so many places where there were stairs and no ramps and even if there were ramps they were probably a bit more than the 1:12 which is the advice given. I have heard that this year s venue is also a bit challenging in terms of accessibility for differently-abled people. I am clueless as to did differently-able find debconf16 in terms of accessibility or not ? A related query to that one, if a Debconf s final report mentions issues with accessibility, do the venues make any changes so that at some future date, differently-abled people would have a better time. I know of Indian institutions reluctance to change, to do expenditure, dunno how western countries do it. Any ideas, comments are welcome.
Filed under: Miscellenous Tagged: #386, #accessibility, #air-travel, #Computers, #differently-abled, #Railways, gaming

11 February 2017

Niels Thykier: On making Britney smarter

Updating Britney often makes our life easier. Like: Concretely, transitions have become a lot easier. When I joined the release team in the summer 2011, about the worst thing that could happen was discovering that two transitions had become entangled. You would have to wait for everything to be ready to migrate at the same time and then you usually also had to tell Britney what had to migrate together. Today, Britney will often (but not always) de-tangle the transitions on her own and very often figure out how to migrate packages without help. The latter is in fact very visible if you know where to look. Behold, the number of manual easy and hint -hints by RT members per year[2]:
Year   Total   easy   hint
-----+-------+------+-----
2005     53      30    23 
2006    146      74    72
2007     70      40    30
2008    113      68    45
2009    229     171    58
2010    252     159    93
2011    255     118   137
2012     29      21     8
2013     36      30     6
2014     20      20     0
2015     25      17     8
2016     16      11     5
2017      1       1     0
As can be seen, the number of manual hints drop by factor of ~8.8 between 2011 and 2012. Now, I have not actually done a proper statistical test of the data, but I have a hunch that drop was significant (see also [3] for a very short data discussion). In conclusion: Smooth-updates (which was enabled late in 2011) have been a tremendous success.  [1] A very surprising side-effect of that commit was that the ( original ) auto-hinter could now solve a complicated haskell transition. Turns out that it works a lot better, when you give correct information!  [2] As extracted by the following script and then manually massaged into an ASCII table. Tweak the in-line regex to see different hints.
respighi.d.o$ cd "/home/release/britney/hints" && perl -E '
    my (%years, %hints);
    while(<>)   
        chomp;
        if (m/^\#\s*(\d 4 )(?:-?\d 2 -?\d 2 );/ or m/^\#\s*(?:\d+-\d+-\d+\s*[;:]?\s*)?done\s*[;:]?\s*(\d 4 )(?:-?\d 2 -?\d 2 )/)  
             $year = $1; next;
          
         if (m/^((?:easy hint) .*)/)  
             my $hint = $1; $years $year ++ if defined($year) and not $hints $hint ++;
             next;
          
         if (m/^\s*$/)   $year = undef; next;  
     ;
    for my $year (sort(keys(%years)))   
        my $count = $years $year ;
        print "$year: $count\n"
     ' * OLD/jessie/* OLD/wheezy/* OLD/Lenny/* OLD/*
[3] I should probably mention for good measure that extraction is ignoring all hints where it cannot figure out what year it was from or if it is a duplicate. Notable it is omitting about 100 easy/hint-hints from OLD/Lenny (compared to a grep -c), which I think accounts for the low numbers from 2007 (among other). Furthermore, hints files are not rotated based on year or age, nor am I sure we still have all complete hints files from all members.
Filed under: Debian, Release-Team

2 February 2017

Paul Wise: FLOSS Activities January 2017

Changes

Issues

Review

Administration
  • Debian: reboot 1 non-responsive VM, redirect 2 users to support channels, redirect 1 contributor to xkb upstream, redirect 1 potential contributor, redirect 1 bug reporter to mirror team, ping 7 folks about restarting processes with upgraded libs, manually restart the sectracker process due to upgraded libs, restart the package tracker process due to upgraded libs, investigate failures connecting to the XMPP service, investigate /dev/shm issue on abel.d.o, clean up after rename of the fedmsg group.
  • Debian mentors: lintian/security updates & reboot
  • Debian packages: deploy 2 contributions to the live server
  • Debian wiki: unblacklist 1 IP address, whitelist 10 email addresses, disable 18 accounts with bouncing email, update email for 2 accounts with bouncing email, reported 1 Debian member as MIA, redirect 1 user to support channels, add 4 domains to the whitelist.
  • Reproducible builds: rescheduled Debian pyxplot:amd64/unstable for themill.
  • Openmoko: security updates & reboots.

Debian derivatives
  • Send the annual activity ping mail.
  • Happy new year messages on IRC, forward to the list.
  • Note that SerbianLinux does not provide source packages.
  • Expand URL shortener on SerbianLinux page.
  • Invite PelicanHPC, Netrunner, DietPi, Hamara Linux (on IRC), BitKey to the census.
  • Add research publications link to the census template
  • Fix Symbiosis sources.list
  • Enquired about SalentOS downtime
  • Fixed and removed some 404 BlankOn links (blog, English homepage)
  • Fixed changes to AstraLinux sources.list
  • Welcome Netrunner to the census

Sponsors I renewed my support of Software Freedom Conservancy. The openchange 1:2.2-6+deb8u1 upload was sponsored by my employer. All other work was done on a volunteer basis.

Next.

Previous.